//  /=============================================================/
//  |   Auteurs  : J.JULLIEN / R.HERLEMAN / R.CHAILAN             |
//  |   Fichier  : clause.c                                       |
//  |   Date     : 12/04/2009                                     |
//  |   Objet    : Définition du type "t_Clause" &                |
//  |              ses fonctions associées                        |
//  /=============================================================/

#include "clause.h"

/* ------------------------------------------------------------------------ */
/* -------------------- Définition fonctions exportées -------------------- */
/* ------------------------------------------------------------------------ */

t_Clause clauseInit (int num) {
  t_Clause c;
  
  c.numClause = num;
  c.etat = INCHANGEE;
  c.litteral = NULL;
  c.dernierLitteral = NULL;
  
  c.nbVariables = 0;
  c.nbNeutres = 0;
  c.nbFalsifies = 0;
  c.nbSatisfaits = 0;
  
  c.hashPred = NULL;
  c.hashSuiv = NULL;
  
  return c;
}

void clauseMAJCompteurs (t_Clause* c, t_Litteral l,
                         int ancienneVal, int nouvelleVal) {
  if (litteralGetValeur(l, ancienneVal) == 0) {
    c->nbFalsifies--;
  } else {
    if (litteralGetValeur(l, ancienneVal) == 1) {
      c->nbSatisfaits--;
    } else {
      c->nbNeutres--;
    }
  }
  
  if (litteralGetValeur(l, nouvelleVal) == 0) {
    c->nbFalsifies++;
  } else {
    if (litteralGetValeur(l, nouvelleVal) == 1) {
      c->nbSatisfaits++;
    } else {
      c->nbNeutres++;
    }
  }
  
  if (c->nbSatisfaits != 0) {
    c->etat = SATISFAITE;
  } else {
    if (c->nbFalsifies == c->nbVariables) {
      c->etat = FALSIFIEE;
    } else {
      if (c->nbNeutres == c->nbVariables) {
        c->etat = INCHANGEE;
      } else {
        c->etat = RACCOURCIE;
      }
    }
  }
}

int clauseEstVide (t_Clause c) {
  return c.litteral == NULL; 
}

void clauseAjouterLitteral (t_Clause* c, t_Litteral* lit) {
  if (clauseEstVide(*c)) {
    c->litteral = lit;
  } else {
    c->dernierLitteral->variableSuiv = lit;
  }
  c->dernierLitteral = lit;
  c->nbNeutres++;
  c->nbVariables++;
}

t_Litteral* clauseGetLitteral(t_Clause c) {
  return c.litteral;
}

void clauseAfficherLigne(t_Clause clause) {
  int j;
  printf("%d | ", clause.numClause+1);
  t_Litteral *c = clauseGetLitteral(clause);
  int varLues = 0;
  if (c != NULL) {
    for (j = 0; j < c->variable; j++) {
      printf("  ");
      varLues++;
    }
  }
  while (c != NULL) {
    litteralAfficherSigne(*c);
    varLues++;
    
    c = c->variableSuiv;
    
    if (c != NULL) {
      for (j = varLues; j < c->variable; j++) {
        printf("  ");
        varLues++;
      }
    }
  }
}

void clauseAfficherEnsemble(t_Clause clause) {
  t_Litteral *c = clauseGetLitteral(clause);
  printf("{");
  while (c != NULL) {
    litteralAfficherPredicat(*c);      
    if ((*c).variableSuiv) {
      printf(", ");
    }
    c = (*c).variableSuiv;
  }
  printf("}");
}

void clauseAfficherFormule(t_Clause clause) {
  t_Litteral *c = clauseGetLitteral(clause);
  printf("(");
  while (c != NULL) {
    litteralAfficherPredicat(*c);      
    if ((*c).variableSuiv) {
      printf(" ∨ ");
    }
    c = (*c).variableSuiv;
  }
  printf(")"); 
}

void clauseAfficherDebug (t_Clause c) {
  printf("Clause %d\n", c.numClause);
  
  char *tabEtat[10] = { "SATISFAITE", "FALSIFIEE", "INCHANGEE", "RACCOURCIE"} ;
  printf("  Etat : %s\n", tabEtat[c.etat]);
  printf("  NbVariables : %d\n", c.nbVariables);
  printf("  NbNeutres : %d\n", c.nbNeutres);
  printf("  NbSatisfaits : %d\n", c.nbSatisfaits);
  printf("  NbFalsifiés : %d\n", c.nbFalsifies);
  printf("\n  Litteraux : ");
  t_Litteral *l = clauseGetLitteral(c);
  while (l != NULL) {
    litteralAfficherDebug(*l, 0, 0);
    l = l->variableSuiv;
  }
  printf("\n");
}

